<html>
<head><meta charset="utf-8"><title>desugaring projections in chalk · wg-traits · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/index.html">wg-traits</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/desugaring.20projections.20in.20chalk.html">desugaring projections in chalk</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="179333620"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/desugaring%20projections%20in%20chalk/near/179333620" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/desugaring.20projections.20in.20chalk.html#179333620">(Oct 29 2019 at 14:27)</a>:</h4>
<p>So I realized something this morning. While I still like the idea of desugaring projections, it's really equivalent to eager normalization -- and it has some of the same problems! In particular, it is straightforward to handle something like this:</p>
<div class="codehilite"><pre><span></span>Implemented(T: Foo&lt; &lt;T as Iterator&gt;::Item &gt;)
</pre></div>


<p>to</p>
<div class="codehilite"><pre><span></span>Implemented(T: Foo&lt; U &gt;) :- ProjectionEq(&lt;T as Iterator&gt;::Item  = U)
</pre></div>


<p>But we can't really normalize something like this that way:</p>
<div class="codehilite"><pre><span></span>Implemented(T: Foo&lt; for&lt;&#39;a&gt; fn(&lt;&amp;&#39;a as Bar&gt;::Item &gt;)
</pre></div>


<p>The problem is that the result <code>U</code> might have to name <code>'a</code>. This is of course a known bug in rustc. It works fine in chalk today, though, because we basically <em>do</em> the <code>ProjectionEq</code> desugaring, but quite "late", such that we create the <code>ProjectionEq</code> in a context where it is allowed to name <code>'a</code>.</p>
<p>This doesn't really invalidate much of the work towards introducing type families etc -- that work is still needed to enable chalk to be shared between rustc and rust-analyzer, for example, and I still think it can be very useful for doing quality engineering later. But it does sort of mean that the "desugaring" plan doesn't make sense as I imagined it -- I'm not sure if there is some alternative formulation that <em>does</em> make sense, to be honest. </p>
<p>All of this fits well with our plan for next design meeting, since the stuff I had planned to talk about was exactly more details around how we handle cases like this (and how to help catch rustc up with chalk in some respects).</p>



<a name="179333841"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/desugaring%20projections%20in%20chalk/near/179333841" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/desugaring.20projections.20in.20chalk.html#179333841">(Oct 29 2019 at 14:29)</a>:</h4>
<p>Interestingly, I had already written the code to do the transformation on a branch -- it included an <code>unwrap</code> call that would have failed for these higher-ranked constructs that I say we can't handle. That unwrap never failed. This suggests a hole in our test coverage we should probably fix. :)</p>



<a name="179333976"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/desugaring%20projections%20in%20chalk/near/179333976" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/desugaring.20projections.20in.20chalk.html#179333976">(Oct 29 2019 at 14:30)</a>:</h4>
<blockquote>
<p>I'm not sure if there is some alternative formulation that <em>does</em> make sense, to be honest. </p>
</blockquote>
<p>I guess the alternative formulation might be to "lower" more of the equality rules, particularly those around higher-ranked types, into goals themselves. I'm not sure if there is real value there or not.</p>



<a name="179340855"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/desugaring%20projections%20in%20chalk/near/179340855" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> detrumi <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/desugaring.20projections.20in.20chalk.html#179340855">(Oct 29 2019 at 15:32)</a>:</h4>
<p>I'm not sure I understand, isn't this possible?</p>
<div class="codehilite"><pre><span></span>Implemented(T: Foo&lt; U &gt;) :- ProjectionEq(for&lt;&#39;a&gt; fn(&lt;&amp;&#39;a as Bar&gt;::Item) = U)
</pre></div>



<a name="179341239"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/desugaring%20projections%20in%20chalk/near/179341239" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> detrumi <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/desugaring.20projections.20in.20chalk.html#179341239">(Oct 29 2019 at 15:36)</a>:</h4>
<p>Or is it the left <code>U</code> that might have to name <code>'a</code>?</p>



<a name="179364055"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/desugaring%20projections%20in%20chalk/near/179364055" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/desugaring.20projections.20in.20chalk.html#179364055">(Oct 29 2019 at 19:16)</a>:</h4>
<p><span class="user-mention" data-user-id="125131">@detrumi</span> what you wrote there is not directly possible just by the structure of our goals, but you could write something like</p>
<div class="codehilite"><pre><span></span>forall&lt;T, U&gt; { // let me make these explicit, I left them implicit before
    Implemented(T: Foo&lt; fn(U) &gt;) :-
        forall&lt;&#39;a&gt; { ProjectionEq(&lt;&amp;&#39;a as Bar&gt;::Item = U) }
}
</pre></div>


<p>Unfortunately, as you noted, the problem here is that the <code>U</code> might have to name <code>'a</code> -- ie., you could have</p>
<div class="codehilite"><pre><span></span><span class="k">impl</span><span class="o">&lt;</span><span class="n">T</span><span class="o">&gt;</span><span class="w"> </span><span class="n">Bar</span><span class="w"> </span><span class="k">for</span><span class="w"> </span><span class="n">T</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">    </span><span class="k">type</span> <span class="nc">Item</span><span class="w"> </span><span class="o">=</span><span class="w"> </span><span class="n">T</span><span class="p">;</span><span class="w"></span>
<span class="p">}</span><span class="w"></span>
</pre></div>


<p>and (as you can see) <code>'a</code> is not in scope at the point where <code>U</code> is declared.</p>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>